Consider the TRS R consisting of the rewrite rules
1:
purge(nil)
→ nil
2:
purge(x . y)
→ x . purge(remove(x,y))
3:
remove(x,nil)
→ nil
4:
remove(x,y . z)
→ if(x = y,remove(x,z),y . remove(x,z))
There are 3 dependency pairs:
5:
PURGE(x . y)
→ PURGE(remove(x,y))
6:
PURGE(x . y)
→ REMOVE(x,y)
7:
REMOVE(x,y . z)
→ REMOVE(x,z)
The approximated dependency graph contains one SCC:
{7}.
Consider the SCC {7}.
There are no usable rules.
By taking the AF π with
π(REMOVE) = 2
and π(.) = [2] together with
the lexicographic path order with
empty precedence,
rule 7
is strictly decreasing.